| Definitions | first(e), pred(e), pred!(e;e'), SWellFounded(R(x;y)), kind(e), loc(e), constant_function(f;A;B), r  s, val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time),  ,  , Msg(M), kindcase(k; a.f(a); l,t.g(l;t) ),   x. t(x), EState(T), EOrderAxioms(E; pred?; info), Unit, EqDecider(T), x,y. t(x;y), {T}, x.A(x), locl(a), Knd, IdLnk, f**(e), loc(e), t.1, let x,y = A in B(x;y), (e < e'), e < e', (e <loc e'), y=f*(x) via L, y is f*(x), False, !Void(),  , strong-subtype(A;B), a:A fp B(a), e c e', f(a), Top, no_repeats(T;l), (x  l), adjacent(T;L;x;y), e loc e' , L1  L2, hd(l), P & Q, P   Q,  A, a < b, P  Q, Id,  x:A. B(x), {x:A| B(x)} , left + right,  b, x:A  B(x), chain-consistent(f;chain), type List,  x:A. B(x), E, <a, b>, E(X), sys-antecedent(es;Sys), x:A B(x),  , AbsInterface(A), Type, ES, t T, s = t, ||as||, Y, rec-case(a) of [] => s | x::y => z.t(x;y;z), n+m, last(L), l[i], nth_tl(n;as), if b then t else f fi , case b of inl(x) => s(x) | inr(y) => t(y), if a<b then c else d, n - m, tl(l), {i..j },  , i j < k, A B, can-apply(f;x), isl(x), Atom$n, rcv?(e), ecase1(e;info;i.f(i);l,e'.g(l;e')), sender(e),  , Ax, link(e), R^+,  , rel_exp(T; R; n), int_eq(a; b; c; d), outl(x), token{$token:t}, destination(l), pi2(t), source(l), x,y:A//B(x;y), b-union(A; B), int_nzero, nequal(T; a; b), isint(z; a; b), multiply(n; m), islocal(k), inr x , rcv(l; tg), inl x , actof(k), outr(x), state_when(e; info; pred?; init; Trans; val; time), when-after(e; info; pred?; init; Trans; val; time), let(a; x.b(x)), es-shift(s; r), qadd(r; s), qsub(r; s), qmul(r; s), -n, isrcv(k), lnk(k), tagof(k), a b, grp_le(g), qadd_grp, qpositive(r),  x:A.B(x), es-pred?(es), es_info(es), p  q, p  q, p q, b, e = e', deq-member(eq;x;L), a = b, a = b, qeq(r;s), q_less(a;b), q_le(r;s), eq_atom$n(x;y), [d], a < b, x f y, a < b, null(as), x =a y, (i = j), i z j, i <z j, p =b q, e X, e(e1,e2].P(e), e[e1,e2].P(e), e[e1,e2].P(e), e[e1,e2).P(e), e[e1,e2).P(e), ee'.P(e), e<e'. P(e), ee'.P(e), e<e'.P(e), Dec(P), SQType(T), s ~ t, True,  T, tt, ff, f(x)?z, P  Q, P Q, f g, IsPrimeIdeal(R;P), IsIntegDom(r), IsMonHom{M1,M2}(f), IsGroup(T;op;id;inv), IsMonoid(T;op;id), monot(T;x,y.R(x;y);f), Cancel(T;S;op), FunThru2op(A;B;opa;opb;f), fun_thru_1op(A;B;opa;opb;f), Dist1op2opLR(A;1op;2op), IsAction(A;x;e;S;f), IsBilinear(A;B;C;+a;+b;+c;f), BiLinear(T;pl;tm), Inverse(T;op;id;inv), Comm(T;op), Assoc(T;op), Ident(T;op;id), CoPrime(a,b), Connex(T;x,y.R(x;y)), AntiSym(T;x,y.R(x;y)), Trans(T;x,y.E(x;y)), Sym(T;x,y.E(x;y)), Refl(T;x,y.E(x;y)), IsEqFun(T;eq), Inj(A;B;f), InvFuns(A;B;f;g), a =!x:T. Q(x), SqStable(P), l_disjoint(T;l1;l2), Outcome, q-rel(r;x), r < s, (xL.P(x)), xL. P(x), A c B, a < b, a <p b, a b, a ~ b, b | a, x <<= y, as @ bs, (last change to x before e), lastchange(x;e), es-first-from(es;e;l;tg), isrcv(e), es-init(es;e), x << y, pred(e), first(e), kind(e), @e(x v), e(e1,e2].P(e), increasing(f;k), X(e), #$n, t ...$L |
| Lemmas | adjacent wf, and functionality wrt iff, sublist wf, es-le-not-locl, es-locl irreflexivity, es-le weakening eq, chain-order-le antisymmetry, rev implies wf, iff wf, es-locl-iff, implies functionality wrt iff, all functionality wrt iff, es-first wf, es-loc-pred, squash wf, es-le-loc, es-isrcv-loc, Id sq, chain-path-ordered, decidable assert, sq stable from decidable, bfalse wf, btrue wf, true wf, es-is-interface wf, false wf, guard wf, decidable equal es-E-interface, fun-connected-step, fun-connected transitivity, decidable es-locl, es-locl transitivity2, es-causl weakening, es-locl-antireflexive, subtype rel wf, sys-antecedent wf, es-E-interface wf, member wf, es-E wf, assert wf, es-E-interface-subtype rel, not wf, fun-connected wf, fun-path wf, es-le wf, es-locl wf, es-causl wf, es-loc wf, Id wf, fun-connected-induction, chain-consistent wf, event system wf, deq wf, unit wf, IdLnk wf, EOrderAxioms wf, EState wf, Knd wf, kindcase wf, Msg wf, nat wf, rationals wf, val-axiom wf, cless wf, qle wf, bool wf, constant function wf, top wf, es-interface wf, es-causle wf, strongwellfounded wf, pred! wf, loc wf |
